[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
data asm specification
awbuf
using awbuf-inv,
address
,
ebm-vol-inv
,
lp-array
procedures awbuf_get_volume_size# address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : : nat ;
awbuf_get_buf# address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : : bufleb ;
awbuf_is_readonly# address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : : bool ;
awbuf_enter_readonly# address × nat × nat-list × avolume × lp-array × nat-set × bufleb : : bool ;
awbuf_move_buf# nat × nat × address × nat × nat-list × avolume × lp-array × nat-set × bool : bufleb : error nondeterministic;
awbuf_destroy_buf# address × nat × nat-list × avolume × lp-array × nat-set × bool : bufleb : error ;
awbuf_write_buf# nat × buffer × address × nat × nat-list × lp-array × nat-set × bufleb : avolume × bool : error nondeterministic;
awbuf_commit# lp-array × address × nat × avolume × bufleb : nat-set × address × nat × nat-list × lp-array × nat-set × bool : error
nondeterministic;
awbuf_requires_commit# address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : : bool nondeterministic;
awbuf_add_log_leb# nat × nat × address × nat × avolume × lp-array × nat-set × bool : nat-list × bufleb : error nondeterministic;
awbuf_read_buf# nat × nat × nat × address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : buffer : error
nondeterministic;
awbuf_remap# nat × address × nat × nat-list × lp-array × nat-set × bufleb × bool : avolume : error nondeterministic;
awbuf_unmap# nat × address × nat × nat-list × lp-array × nat-set × bufleb × bool : avolume nonfunctional ;
awbuf_get_page_size# address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : : nat ;
awbuf_get_leb_size# address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool : : nat ;
awbuf_format#
nat × nat × lp-array × address × nat : : address × nat × nat-list × avolume × lp-array × nat-set × bufleb × bool × error
nondeterministic;
awbuf_recover#
: address × nat × nat-set × nat-list × lp-array × address × nat × nat-list × lp-array × nat-set × avolume : bufleb × bool × error
nondeterministic;
variables WVOL : avolume flexible;
BUF : buffer flexible;
BUF0 : buffer flexible;
N : nat flexible;
N0 : nat flexible;
N1 : nat flexible;
LNUM : nat flexible;
OFFSET : nat flexible;
SIZE : nat flexible;
ISBUF : bool flexible;
isbuf : bool;
ERR : error flexible;
ERR0 : error flexible;
VOLSIZE : nat flexible;
WROOTADR : address flexible;
WROOTADR0 : address flexible;
WMAXINO : nat flexible;
WMAXINO0 : nat flexible;
COMMIT? : bool flexible;
LOG : nat-list flexible;
WLOG : nat-list flexible;
LPT : lp-array flexible;
WLPT : lp-array flexible;
ORPHANS : nat-set flexible;
WORPHANS : nat-set flexible;
WBUFLEB : bufleb flexible;
WBUFLEB0 : bufleb flexible;
AROFS : bool flexible;
AROFS0 : bool flexible;
state variables WROOTADR : address flexible;
WMAXINO : nat flexible;
WLOG : nat-list flexible;
WVOL : avolume flexible;
WLPT : lp-array flexible;
WORPHANS : nat-set flexible;
WBUFLEB : bufleb flexible;
AROFS : bool flexible;
initialization procedure awbuf_format#
if ERR = ESUCCESS
sequential
invariants inv : ⊦ awbuf-inv(WVOL, WBUFLEB);
lpt-size : ⊦ # WLPT = # WVOL;
crash predicate WROOTADR = WROOTADR` ∧ WMAXINO = WMAXINO` ∧ WLOG = WLOG` ∧ WLPT = WLPT` ∧ WVOL ↓ WVOL` ∧ WORPHANS = WORPHANS`
with crash-neutrality
introducing synchronized predicate
synced(WVOL)
recovery procedure awbuf_recover#
if ERR = ESUCCESS
declarations get-volume-size:
awbuf_get_volume_size#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; N)
precondition true;
postcondition true;
{N := # WVOL
}
get-buf:
awbuf_get_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; WBUFLEB0)
precondition true;
postcondition true;
{WBUFLEB0 := WBUFLEB
}
is-readonly:
awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; AROFS0)
precondition true;
postcondition true;
{AROFS0 := AROFS
}
enter-readonly:
awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS)
precondition true;
postcondition true;
{AROFS := true
}
move-buf:
awbuf_move_buf#(LNUM, OFFSET, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, AROFS; WBUFLEB; ERR)
precondition WBUFLEB = buffered(LNUM)
∨ (WBUFLEB = nobuffer ∨ is-aligned(# WVOL[WBUFLEB.leb].data, EB_PAGE_SIZE)) ∧ LNUM < # WVOL
∧ WVOL[LNUM].mapped? ∧ OFFSET = # WVOL[LNUM].data
;
postcondition true;
{if WBUFLEB = buffered(LNUM)
∨ (WBUFLEB = nobuffer ∨ is-aligned(# WVOL[WBUFLEB.leb].data, EB_PAGE_SIZE)) ∧ LNUM < # WVOL ∧ WVOL[LNUM].mapped?
∧ OFFSET = # WVOL[LNUM].data
then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then WBUFLEB := buffered(LNUM)}
else abort
}
destroy-buf:
awbuf_destroy_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, AROFS; WBUFLEB; ERR)
precondition synced(WVOL);
postcondition true;
{if synced(WVOL) then if AROFS then ERR := EROFS else WBUFLEB := nobuffer, ERR := ESUCCESS else abort
}
write-buf:
awbuf_write_buf#(N, BUF, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; WVOL, AROFS; ERR)
precondition WBUFLEB ≠ nobuffer ∧ # WVOL[WBUFLEB.leb].data + N ≤ LEB_SIZE ∧ N ≤ # BUF;
postcondition true;
{if WBUFLEB ≠ nobuffer ∧ # WVOL[WBUFLEB.leb].data + N ≤ LEB_SIZE ∧ N ≤ # BUF
then if AROFS
then ERR := EROFS
else {fail_or_success#(; ; ERR);
let LNUM = WBUFLEB.leb
in if ERR = ESUCCESS
then WVOL[LNUM] := mapped(WVOL[LNUM].data + subarray(BUF, 0, N))
else { choose N0
with N0 ≠ 0 ∧ N0 < N ∧ is-aligned(# WVOL[LNUM].data + N0, EB_PAGE_SIZE)
in WVOL[LNUM] := mapped(WVOL[LNUM].data + subarray(BUF, 0, N0))
ifnone skip
or skip;
AROFS := true}}
else abort
}
commit:
awbuf_commit#(LPT, WROOTADR0, WMAXINO0, WVOL, WBUFLEB; ORPHANS, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, AROFS; ERR)
precondition synced(WVOL) ∧ # LPT = # WVOL;
postcondition true;
{if synced(WVOL) ∧ # LPT = # WVOL
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then {WROOTADR := WROOTADR0; WMAXINO := WMAXINO0; WLOG := []; WLPT := LPT; WORPHANS := ORPHANS}
else AROFS := true;
ORPHANS := ?}
else abort
}
requires-commit:
awbuf_requires_commit#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; COMMIT?)
precondition true;
postcondition true;
{COMMIT? := ?
}
add-log-leb:
awbuf_add_log_leb#(LNUM, OFFSET, WROOTADR, WMAXINO, WVOL, WLPT, WORPHANS, AROFS; WLOG, WBUFLEB; ERR)
precondition LNUM < # WVOL ∧ WVOL[LNUM].mapped? ∧ OFFSET = # WVOL[LNUM].data ∧ synced(WVOL);
postcondition true;
{if LNUM < # WVOL ∧ WVOL[LNUM].mapped? ∧ OFFSET = # WVOL[LNUM].data ∧ synced(WVOL)
then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then WLOG := WLOG + LNUM, WBUFLEB := buffered(LNUM)}
else abort
}
read-buf:
awbuf_read_buf#(LNUM, OFFSET, N, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; BUF; ERR)
precondition LNUM < # WVOL ∧ N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE ∧ WVOL[LNUM].mapped?;
postcondition true;
{if LNUM < # WVOL ∧ N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE ∧ WVOL[LNUM].mapped?
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then BUF := copy(WVOL[LNUM].data + mkempbuf(LEB_SIZE - # WVOL[LNUM].data), OFFSET, BUF, 0, N)
else choose BUF0 with # BUF0 = # BUF ∧ range=(BUF0, N, BUF, N, # BUF - N) in BUF := BUF0}
else abort
}
remap:
awbuf_remap#(LNUM, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; WVOL; ERR)
precondition synced(WVOL) ∧ LNUM < # WVOL ∧ buffered(LNUM) ≠ WBUFLEB;
postcondition true;
{if synced(WVOL) ∧ LNUM < # WVOL ∧ buffered(LNUM) ≠ WBUFLEB
then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then WVOL[LNUM] := mapped(mkbuf(0)) else {skip or WVOL[LNUM] := unmapped}}
else abort
}
unmap:
awbuf_unmap#(LNUM, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; WVOL)
precondition synced(WVOL) ∧ LNUM < # WVOL ∧ buffered(LNUM) ≠ WBUFLEB;
postcondition true;
{if synced(WVOL) ∧ LNUM < # WVOL ∧ buffered(LNUM) ≠ WBUFLEB then WVOL[LNUM] := unmapped else abort
}
get-page-size:
awbuf_get_page_size#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; N)
precondition true;
postcondition true;
{N := EB_PAGE_SIZE
}
get-leb-size:
awbuf_get_leb_size#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; N)
precondition true;
postcondition true;
{N := LEB_SIZE
}
format:
awbuf_format#(VOLSIZE, SIZE, LPT, WROOTADR0, WMAXINO0; ; WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS, ERR)
precondition # LPT = VOLSIZE ∧ SIZE = LEB_SIZE;
postcondition true;
{if # LPT = VOLSIZE ∧ SIZE = LEB_SIZE
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then {WVOL := fill(mkavolume(VOLSIZE), unmapped); WROOTADR := WROOTADR0; WMAXINO := WMAXINO0; WLOG := []; WLPT := LPT;
WORPHANS := ∅; WBUFLEB := nobuffer; AROFS := false}
else WVOL := ?, WBUFLEB := ?, AROFS := ?, WROOTADR := ?, WMAXINO := ?, WLOG := ?, WLPT := ?, WORPHANS := ?}
else abort
}
recover:
awbuf_recover#(; WROOTADR0, WMAXINO0, ORPHANS, LOG, LPT, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WVOL; WBUFLEB, AROFS, ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then WBUFLEB := nobuffer, AROFS := false, WROOTADR0 := WROOTADR, WMAXINO0 := WMAXINO, LOG := WLOG, LPT := WLPT, ORPHANS := WORPHANS
else WVOL := ?, WBUFLEB := ?, AROFS := ?, WROOTADR := ?, WMAXINO := ?, WLOG := ?, WLPT := ?, WROOTADR0 := ?, WMAXINO0 := ?, LOG := ?,
LPT := ?, ORPHANS := ?, WORPHANS := ?}
}
end data asm specification